@book{SAT,
  title={Handbook of Satisfiability},
  editor={A. Biere and M. Heule and H. Van Maaren and T. Walsh},
  year=2009,
  publisher={{IOS} Press},
  }

@book{mlcs,
  title={Mathematical Logic for Computer Science (Third Edition)},
  author={M. Ben-Ari},
  publisher={Springer},
  year=2012,
}

@inbook{mlm,
   Author = {Marques-Silva, J. P. and Lynce, I. and Malik, S.},
   Title = {Conflict-Driven Clause Learning SAT Solvers},
   Chapter = {4},
   Pages = {131--153},
   Crossref = {SAT}
}

@inbook{bmc,
   Author = {Biere, A.},
   Title = {Bounded Model Checking},
   Chapter = {14},
   Pages = {457--481},
   Crossref = {SAT}
}

@inbook{cnf,
   Author = {Prestwich, S.},
   Title = {CNF Encodings},
   Chapter = {2},
   Pages = {75--97},
   Crossref = {SAT}
}

@article{mz,
 author = {Malik, S. and Zhang, L.},
 title = {Boolean satisfiability from theoretical hardness to practical success},
 journal = {Commun. ACM},
 volume = {52},
 number = {8},
 year = {2009},
 pages = {76--82},
} 

@inproceedings{ms,
 author = {Marques-Silva, J. P. and Sakallah, K. A.},
 title = {GRASP---a new search algorithm for satisfiability},
 booktitle = {Proceedings of the 1996 IEEE/ACM International Conference on Computer-Aided Design},
 series = {ICCAD '96},
 year = {1996},
 pages = {220--227},
}

@article{nadel,
 author = {Nadel, B.A.},
 title = {Representation Selection for Constraint Satisfaction: A Case Study Using n-Queens},
 journal = {IEEE Expert: Intelligent Systems and Their Applications},
 volume = {5},
 issue = {3},
 month = {June},
 year = {1990},
 pages = {16--23},
} 

@article{primer,
 author = {Ben-Ari, M.},
 title = {A primer on model checking},
 journal = {ACM Inroads},
 issue_date = {March 2010},
 volume = {1},
 number = {1},
 pages = {40--47},
} 
